functor TransAsst (S : TRANSASST_STRUCTS) : TRANSASST = 
struct
  open S

  val localDebug = ref false
  structure F = Frame
  structure E = Env
  structure I = F.Ir
  structure A = F.Assem

  structure D = DebugPrint
  fun mapToMem id = 0 

  fun inEnv (id, env) =
      case env
       of [] => false
        | x :: xs => 
          if x = id
          then true
          else (inEnv (id, xs))
  fun empEnv () = []

  fun entEnv (id, env) = id :: env

  fun transType ty = 
      case ty
       of I.Int => A.Int
        | I.Bool => A.Int
        | I.Struct s => A.Str s
        | I.Pointer t => A.Ptr (transType t)
        | I.Void => A.Wild
        | I.Array (i, t) => (D.showError "transasst.fun : Does not support Array type now!"
                             ; A.Int)

  fun transLval (lv, infunc, lenv, env, senv, st0, st) =
      case lv 
       of I.Var(id, pos) => 
          if inEnv (id, lenv)
          then (A.Id id, E.Simple) 
          else let val elem = E.lookup id env
                   val (islocal, offset, types) = 
                       case elem
                        of SOME(v) => v
                         | NONE => raise Fail "no this case, compiler bug\n"
               in  if islocal 
                   then let val roff = if infunc = 0
                                       then A.Plus(A.Sel(A.getRf st, A.Reg(A.Ebp)), A.IntNum(offset))
                                       else if infunc = 1 orelse infunc = 3
                                       then A.Plus(A.Sel(A.getRf st, A.Reg(A.Esp)), A.IntNum(offset-4*infunc))
                                       else raise Fail "invalid infunc!"
                        in  (fn E.Simple => (A.Sel(A.getHp st, roff), types)
			      | (E.Pointer(tp')) => (A.Sel(A.getHp st, roff), types)
			      | _ => (roff, types)) types
                        end
                   else (fn E.Simple => (A.Sel(A.getHp st, A.Mem(mapToMem(id))), types)
			  | (E.Pointer(tp')) => (A.Sel(A.getHp st, A.Mem(mapToMem(id))), types)
			  | _ => (A.Mem(mapToMem(id)), types)) types
               end
        | I.Ptr(tp, lval, pos) => 
          let val (exp, types) = transLval (lval, infunc, lenv, env, senv, st0, st)
              val rettype = case types
                             of E.Pointer(subtype) => subtype
                              | _ => (raise Fail "impossible"; E.Simple)
          in  (fn E.Simple => (A.Sel(A.getHp st, exp), rettype)
		| (E.Pointer(tp')) => (A.Sel(A.getHp st, exp), rettype)
		| _ => (exp, rettype)) rettype
          end
        | I.Inarray(lval, exp, s_array, pos) => 
          let val (base, types) = transLval (lval, infunc, lenv, env, senv, st0, st)
              val rettype = case types 
                             of E.Array(_, subtype) => subtype
                              | _ => (raise Fail "impossible"; E.Simple)
              val elemSize = E.calTypeSize rettype senv
              val index = transExp (exp, infunc, lenv, env, senv, st0, st)
              val offset = A.Times(index, A.IntNum elemSize)
          in (fn E.Simple => (A.Sel(A.getHp st, A.Plus(base, offset)), rettype)
	       | (E.Pointer(tp')) => (A.Sel(A.getHp st, A.Plus(base, offset)), rettype)
	       | _ => (A.Plus(base, offset), rettype)) rettype 
          end
        | I.Instruct (lval, id, pos) =>
          let val (base, types) = transLval (lval, infunc, lenv, env, senv, st0, st)
              val (offset, rettype) = 
                  case types
                   of  E.Struct(str) => 
                       let val tpopt = E.lookupF str id senv
                       in  case tpopt 
                            of NONE => raise Fail "No such structure or field!"
                             | SOME v => v
                       end
                     | _ => (raise Fail "impossible"; (0, E.Simple)) 
          in (fn E.Simple => (A.Sel(A.getHp st, A.Plus(base, A.IntNum offset)), rettype)
	       | E.Pointer(tp') => (A.Sel(A.getHp st, A.Plus(base, A.IntNum offset)), rettype)
	       | _ => (A.Plus(base, A.IntNum offset), rettype)) rettype
          end
        | I.Instruct2 (lval, id, id2, pos) => 
          let val (base, types) = transLval (lval, infunc, lenv, env, senv, st0, st)
              val (offset, rettype) = 
                  case types
                   of  E.Struct(str) => 
                       let val tpopt = E.lookupF str id senv
                       in  case tpopt 
                            of NONE => raise Fail "No such structure or field!"
                             | SOME v => v
                       end
                     | _ => (raise Fail "impossible"; (0, E.Simple)) 
          in (fn E.Simple => (A.Sel(A.getHp st, A.Plus(base, A.IntNum offset)), rettype)
	       | E.Pointer(tp') => (A.Sel(A.getHp st, A.Plus(base, A.IntNum offset)), rettype)
	       | _ => (A.Plus(base, A.IntNum offset), rettype)) rettype
          end
	| I.Sharp _ => raise Fail "bug"
        | I.Upd (_, _, _) => raise Fail "bug"
        | I.Sel (_, _) => raise Fail "bug"

  and transExp (exp, infunc, lenv, env, senv, st0, st) =
      case exp
       of I.Expvoid => raise Fail "impossible!"
        | I.IntNum i =>  A.IntNum i
        | I.Null => A.IntNum 0
        | I.BinopExp(e1, binop, e2, pos) =>
          let val e1' = (transExp (e1, infunc, lenv, env, senv, st0, st))
              val e2' = (transExp (e2, infunc, lenv, env, senv, st0, st))
          in  case binop
               of I.Plus => A.Plus(e1', e2')
                | I.Minus => A.Minus(e1', e2')
                | I.Times => A.Times(e1', e2')
                | I.Divide => (D.showError "transasst.fun, transExp : Divide is not allowed to appear in a Prop!"
                              ; A.Plus (e1', e2'))
                | I.Modus => (D.showError "transasst.fun, transExp : Modus is not allowed to appear in a Prop!"
                             ; A.Plus (e1', e2'))
                | I.Band => raise Fail "impossible!"
                | I.Bor => raise Fail "impossible!"
                | I.Equ => raise Fail "impossible!"
                | I.NEqu => raise Fail "impossible!"
                | I.GT => raise Fail "impossible!"
                | I.GE => raise Fail "impossible!"
                | I.LT => raise Fail "impossible!"
                | I.LE => raise Fail "impossible!"
          end
        | I.Prev (lv, pos) => #1 (transLval (lv, infunc, lenv, env, senv, st0, st0))
        | I.Lval lv =>  #1 (transLval (lv, infunc, lenv, env, senv, st0, st))
        | I.Result =>  A.Sel(A.getRf st, A.Reg(A.Eax))
                        
        | I.True => raise Fail "impossible!"
        | I.False => raise Fail "impossible!"
        | I.Not (_, _) => raise Fail "impossible!"
        | I.Imply (_, _, _) => raise Fail "impossible!"
        | I.Forall (_, _, _, _) => raise Fail "impossible!"
        | I.Exists (_, _, _, _) => raise Fail "impossible!"
        | I.Pi (_, _) =>   raise Fail "impossible!" 
        | I.N (_, _) => raise Fail "impossible!"
        | I.D (_, _) => raise Fail "impossible!"
        | I.LList (_, _) => raise Fail "impossible!"
        | I.Tree (_, _) => raise Fail "impossible!"
        | I.Pred(_, _, _) => raise Fail "impossible!"
        | I.Let (_, _, _, _) => raise Fail "impossible!"
                                                          
  fun getPlvalType (lenv, env, senv, l) =
      case l
       of I.Var(id, pos) =>  
          let val elem = E.lookup id env
              val _ = if !localDebug
                      then D.debugPrint id
                      else ()
              val (_, _, types) = 
                  case elem
                   of SOME(v) => v
                    | NONE => (D.showWarning "transasst.fun, getPlvalType : bounded variable has type : Env.Simple"
                             ; (true, 0, E.Simple))
          in  types                
          end
        | I.Ptr(t, lv, pos) =>
          let val types = getPlvalType (lenv, env, senv, lv)
              val rettype = case types
                             of E.Pointer(subtype) => subtype
                              | _ => (raise Fail "impossible"; E.Simple)
          in  rettype
          end
        | I.Inarray (lv, e, len, pos) =>
          let val types = getPlvalType (lenv, env, senv, lv)
              val rettype = case types 
                             of E.Array(_, subtype) => subtype
                              | _ => (raise Fail "impossible"; E.Simple)
          in  rettype
          end
        | I.Instruct (lv, id, pos) =>
          let val types = getPlvalType (lenv, env, senv, lv)
              val (offset, rettype) = 
                  case types
                   of  E.Struct(str) => 
                       let val tpopt = E.lookupF str id senv
                       in  case tpopt 
                            of NONE => raise Fail "No such structure or field!"
                             | SOME v => v
                       end
                     | _ => (raise Fail "impossible") 
          in  rettype
          end
        | I.Instruct2 (lv, id, id2, pos) =>
          let val types = getPlvalType (lenv, env, senv, lv)
              val (offset, rettype) = 
                  case types
                   of  E.Struct(str) => 
                       let val tpopt = E.lookupF str id senv
                       in  case tpopt 
                            of NONE => raise Fail "No such structure or field!"
                             | SOME v => v
                       end
                     | _ => (raise Fail "impossible") 
          in  rettype
          end
	| I.Sharp _ => raise Fail "bug"
        | I.Upd (_, _, _) => raise Fail "bug"
        | I.Sel (_, _) => raise Fail "bug"
                                            
  fun transProp (rettype, exp, infunc, lenv, env, senv) st0 st =
      case exp 
       of I.True => A.True
        | I.False => A.Not(A.True)
        | I.BinopExp (e1, binop, e2, pos) =>
          (case binop
            of I.Band => 
               A.And(transProp (rettype, e1, infunc, lenv, env, senv) st0 st, transProp (rettype, e2, infunc, lenv, env, senv) st0 st)
             | I.Bor =>
               A.Or(transProp (rettype, e1, infunc, lenv, env, senv) st0 st, transProp (rettype, e2, infunc, lenv, env, senv) st0 st)
             | I.GT =>
               A.Gt(transExp (e1, infunc, lenv, env, senv, st0, st), transExp (e2, infunc, lenv, env, senv, st0, st))
             | I.GE =>
               A.Ge(transExp (e1, infunc, lenv, env, senv, st0, st), transExp (e2, infunc, lenv, env, senv, st0, st))
             | I.LT =>
               A.Lt(transExp (e1, infunc, lenv, env, senv, st0, st), transExp (e2, infunc, lenv, env, senv, st0, st))
             | I.LE =>
               A.Le(transExp (e1, infunc, lenv, env, senv, st0, st), transExp (e2, infunc, lenv, env, senv, st0, st))
             | I.Equ =>
               A.Eq(transExp (e1, infunc, lenv, env, senv, st0, st), transExp (e2, infunc, lenv, env, senv, st0, st))
             | I.NEqu =>
               A.Ne(transExp (e1, infunc, lenv,  env, senv, st0, st), transExp (e2, infunc, lenv, env, senv, st0, st))
             | I.Plus => (raise Fail "impossible")
             | I.Minus => (raise Fail "impossible")
             | I.Times => (raise Fail "impossible")
             | I.Divide => (raise Fail "impossible")
             | I.Modus => (raise Fail "impossible"))
        | I.Not(e, pos) => A.Not(transProp (rettype, e, infunc, lenv, env, senv) st0 st)
        | I.Imply(e1, e2, pos) =>
          A.Imply(transProp (rettype, e1, infunc, lenv, env, senv) st0 st, transProp (rettype, e2, infunc, lenv, env, senv) st0 st)
        | I.Forall(id, t, e, pos) =>
          let val lenv_new = entEnv (id, lenv)
          in  A.Forall((id, transType t), transProp (rettype, e, infunc, lenv_new, env, senv) st0 st)
          end
        | I.Exists(id, t, e, pos) =>
          let val lenv_new = entEnv (id, lenv)
          in  A.Ex((id, transType t), transProp (rettype, e, infunc, lenv_new, env, senv) st0 st)
          end           
        | I.Expvoid => raise Fail "impossible!"
        | I.IntNum i => raise Fail "impossible!"
        | I.Null => raise Fail "impossible!"
        | I.Prev (lv, pos) => raise Fail "impossible!"
        | I.Lval lv => (D.showError "transasst.fun, transProp : Lvalues should not be used as propositions!"; A.True)
        | I.Result => (D.showError "transasst.fun, transProp : Result should not be used as a proposition!"; A.True)                      
        | I.Pi (ll, pos) => 
          let val newp = I.trPi (ll, pos)
          in  transProp (rettype, newp, infunc, lenv, env, senv) st0 st
          end
        | I.N (l, pos) => 
          let val newp = I.trN (l, pos)
          in  transProp (rettype, newp, infunc, lenv, env, senv) st0 st
          end
        | I.D (l, pos) => 
          let val newp = I.trD (l, pos)
          in  transProp (rettype, newp, infunc, lenv, env, senv) st0 st
          end
        | I.LList (e, pos) => 
          (case e
            of I.Lval lv =>
               let val ls = transExp (e, infunc, lenv, env, senv, st0, st)  
                   val t = getPlvalType (lenv, env, senv, lv)
                   val subt = case t
                               of E.Pointer st => st
                                | _ => raise Fail "should be pointer"
                   val  (size, offset) = 
                        (case subt
                         of E.Struct s => 
                            let val sz = E.calTypeSize subt senv
                                val fl = E.toList (E.lookupFL s senv)
                                fun f [] = NONE
                                  | f ((k, (off, tp)) :: l) = 
                                    (case tp 
                                      of  E.Pointer(E.Struct s') =>
                                          if s = s' 
                                          then SOME off
                                          else f l
                                        | _ => f l)
                                val off = case (f fl)
                                           of  NONE => raise Fail "no next field"
                                             | SOME i => i
                            in  (sz, off) 
                            end
                          | _ => raise Fail "should be structure")
               in  A.List(A.getHp st, ls, size, offset)
               end
             | I.Result =>
               let val ls = A.Some (A.Sel ( A.getRf st, A.Reg (A.Eax)))
                   val t = case rettype
                            of NONE => raise Fail "should not has result here!"
                             | SOME (I.Pointer subt) => subt
                             | _ => raise Fail "should be pointer"
                   val (size, offset) =
                       (case t
                         of I.Struct s =>
                            let val sz = E.calTypeSize (E.Struct s) senv
                                val fl = E.toList (E.lookupFL s senv)
                                fun f [] = NONE
                                  | f ((k, (off, tp)) :: l) = 
                                    (case tp 
                                      of  E.Pointer(E.Struct s') =>
                                          if s = s' 
                                          then SOME off
                                          else f l
                                        | _ => f l)
                                val off = case (f fl)
                                           of NONE => raise Fail "no next field"
                                            | SOME i => i
                            in  (sz, off) 
                            end
                          | _ => raise Fail "should be structure")
               in  A.List (A.getHp st, ls, size, offset)
               end
             | _ => raise Fail "no such case !")
        | I.Tree (e, pos) =>
          (case e
            of I.Lval lv =>
               let val ls = transExp (e, infunc, lenv, env, senv, st0, st)  
                   val t = getPlvalType (lenv, env, senv, lv)
                   val subt = case t
                               of E.Pointer st => st
                                | _ => raise Fail "should be pointer"
                   val  (size, offsetl, offsetr) = 
                        (case subt
                         of  E.Struct s => 
                             let val sz = E.calTypeSize subt senv
                                 val fl = E.toList (E.lookupFL s senv)
                                 fun f [] (off1, off2) = (off1, off2)
                                   | f ((k, (off, tp)) :: l) (off1, off2) = 
                                     (case tp 
                                       of E.Pointer(E.Struct s') =>
                                          if s = s' 
                                          then if off1 = NONE
                                               then (f l (SOME off, off2))
                                               else if off2 = NONE
                                               then (f l (off1, SOME off))
                                               else (D.showWarning "transasst.fun, transProp : too many childs"
                                                   ; (off1, off2))
                                          else f l (off1, off2)
                                        | _ => f l (off1, off2))
                                 val (off1, off2) = 
                                     case (f fl (NONE, NONE))
                                      of (NONE, _) => raise Fail "no left child"
                                       | (_, NONE) => raise Fail "no right child"
                                       | (SOME i, SOME j) => (i, j)
                             in  (sz, off1, off2) 
                             end
                           | _ => raise Fail "should be structure")
               in  A.Tree(A.getHp st, ls, size, offsetl, offsetr)
               end
             | I.Result =>
               let val ls = A.Some (A.Sel(A.getRf st, A.Reg (A.Eax)))
                   val t = case rettype
                            of NONE => raise Fail "should not has result here!" 
                             | SOME (I.Pointer subt) => subt
                             | _ => raise Fail "should be pointer"
                   val (size, offsetl, offsetr) =
                       (case t
                        of I.Struct s =>
                           let val sz = E.calTypeSize (E.Struct s) senv
                               val fl = E.toList (E.lookupFL s senv)
                               fun f [] (off1, off2) = (off1, off2)
                                 | f ((k, (off, tp)) :: l) (off1, off2) = 
                                   (case tp 
                                     of E.Pointer(E.Struct s') =>
                                        if s = s' 
                                        then if off1 = NONE
                                                 then (SOME off, off2)
                                             else if off2 = NONE
                                             then (off1, SOME off)
                                             else (D.showWarning "transasst.fun, transProp : too many childs"
                                                 ; (off1, off2))
                                        else f l (off1, off2)
                                      | _ => f l (off1, off2))
                               val (off1, off2) = 
                                   case (f fl (NONE, NONE))
                                    of (NONE, _) => raise Fail "no left child"
                                     | (_, NONE) => raise Fail "no right child"
                                     | (SOME i, SOME j) => (i, j)
                           in  (sz, off1, off2) 
                           end
                         | _ => raise Fail "should be structure")
               in  A.Tree (A.getHp st, ls, size, offsetl, offsetr)
               end
             | _ => raise Fail "no such case!")
        | I.Pred (id, e, pos) => A.Pred (id, transProp (rettype, e, infunc, lenv, env, senv) st0 st)
        | I.Let (e1, e2, e3, pos) => 
          transProp (rettype, e3, infunc, lenv, env, senv) st0 st
                                                                           
  fun transPlval (infunc, lenv, env, senv, l) =
      case l
        of I.Var(id, pos) =>  
            if inEnv (id, lenv)
            then (A.Pid(id), E.Simple) 
            else let val elem = E.lookup id env
                     val (islocal, offset, types) = 
                         case elem
                          of SOME(v) => v
                           | NONE => raise Fail ("no this case, compiler bug."^
                                                 "(* we have not considered about the situation that"^ 
                                                 "id is bounded by Forall or Exists *)")
                 in  if islocal 
                     then if infunc = 0
                          then (A.Pstk(offset, A.Ebp), types)
                          else if infunc = 1 orelse infunc = 3
                          then (A.Pstk(offset-4*infunc, A.Esp), types)
                          else raise Fail "invalid infunc!"
                     else (A.Pgmem(mapToMem id), types)                
                 end
         | I.Ptr(t, lv, pos) =>
           let val (lv', types) = transPlval (infunc, lenv, env, senv, lv)
               val rettype = case types
                              of E.Pointer(subtype) => subtype
                                 | _ => (raise Fail "impossible"; E.Simple)
           in  (A.Pmem (0, lv', A.PintNum 1), rettype)
           end
         | I.Inarray (lv, e, len, pos) =>
           let val (base, types) = transPlval (infunc, lenv, env, senv, lv)
               val rettype = case types 
                              of E.Array(_, subtype) => subtype
                               | _ => (raise Fail "impossible"; E.Simple)
               val elemSize = E.calTypeSize rettype senv
               val index = case e
                            of I.IntNum i => i
                             | _ => (D.showError ("transasst.fun, tranPval : " ^
                                                  "Now we are only considering about the situation which the array"^
                                                  "index is an immediate number.")
                                   ; 0)
               val offset = index * elemSize
           in  (A.Pmem(offset, base, A.PintNum 1), rettype)
           end
         | I.Instruct (lv, id, pos) =>
           let val (base, types) = transPlval (infunc, lenv, env, senv, lv)
               val (offset, rettype) = 
                   case types
                    of E.Struct str => 
                       let val tpopt = E.lookupF str id senv
                       in  case tpopt 
                            of NONE => raise Fail "No such structure or field!"
                             | SOME v => v
                       end
                     | _ => (raise Fail "impossible") 
           in  (A.Pmem(offset, base, A.PintNum 1), rettype)
           end
         | I.Instruct2 (lv, id1, id2, pos) =>
           let val (base, types) = transPlval (infunc, lenv, env, senv, lv)
               val (offset, rettype) = 
                   case types
                    of E.Struct str => 
                       let val tpopt = E.lookupF str id1 senv
                       in  case tpopt 
                            of NONE => raise Fail "No such structure or field!"
                             | SOME v => v
                       end
                     | _ => (raise Fail "impossible") 
           in  (A.Pmem(offset, base, A.Pvar (A.Pid id2)), rettype)
           end
	 | I.Sharp _ => raise Fail "bug"
         | I.Upd (_, _, _) => raise Fail "bug"
         | I.Sel (_, _) => raise Fail "bug"                                      
                                             
  fun hasLocalId' (lenv, lval) =
      case lval
       of I.Var (id, pos) => inEnv (id, lenv)
        | I.Ptr (t, lv, pos) => hasLocalId' (lenv, lv)
        | I.Sharp t => (D.showError "transasst.fun, hasLocalId' : no this case!"
                       ; false)
        | I.Inarray (lv, exp, i, pos) => (D.showWarning "transasst.fun, hasLocalId' : we have not implemented array."
                                         ; if hasLocalId' (lenv, lv) orelse hasLocalId (lenv, exp)
                                           then true
                                           else false)
        | I.Instruct (lv, id, pos) => hasLocalId' (lenv, lv)
        | I.Instruct2 (lv, id1, id2, pos) => hasLocalId' (lenv, lv)
        | I.Upd (lv, e1, e2) => (D.showError "transasst.fun, hasLocalId' : no this case!"
                                ; false)
        | I.Sel (lv, e) => (D.showError "transasst.fun, hasLocalId' : no this case!"
                           ; false) 

  and hasLocalId (lenv, exp) =
      case exp
       of I.Expvoid => (D.showError "transasst.fun, hasLocalId : impossible case"
                       ; false)
        | I.IntNum i => false
        | I.True => false
        | I.False => false
        | I.Null => false
        | I.Lval l => hasLocalId' (lenv, l)
        | I.BinopExp (e1, binop, e2, pos) => if hasLocalId (lenv, e1) orelse hasLocalId (lenv, e2)
                                              then true
                                              else false
        | I.Not (e, pos) => hasLocalId (lenv, e)
                             
        | I.Result => false
        | I.Imply (e1, e2, pos) => if hasLocalId (lenv, e1) orelse hasLocalId (lenv, e2)
                                    then true
                                    else false
        | I.Forall (id, t, e, pos) => hasLocalId (lenv, e)
        | I.Exists (id, t, e, pos) => hasLocalId (lenv, e)
        | I.Pi (ll, pos) =>
          let fun f lv = hasLocalId' (lenv, lv)
              fun g l = List.exists f l
          in  List.exists g ll
          end
        | I.N (l, pos) => 
          let fun f lv = hasLocalId' (lenv, lv) 
          in  List.exists f l
          end
        | I.D (l, pos) => 
          let fun f lv = hasLocalId' (lenv, lv)
          in  List.exists f l
          end
        | I.Prev (l, pos) => hasLocalId' (lenv, l)
        | I.LList (e, pos) => hasLocalId (lenv, e)
        | I.Tree (e, pos) => hasLocalId (lenv, e)
        | I.Pred (id, e, pos) => (D.showWarning "transasst.fun, hasLocalId : working in progress now"
                                 ; false)
        | I.Let (e1, e2, e3, pos) => hasLocalId (lenv, e3)
                                     
  fun findPprop (rettype : I.mytype option, 
                 inlocal : bool,                 
                 lenv, 
                 env :(bool * int * Env.types) E.env, 
                 senv : (int * Env.types)E.struct_env,
                 prop : I.exp ) : I.exp * bool =
      case prop
       of I.Pi (ll, pos) => (I.Pi (ll, pos), true)
        | I.N (l, pos) => (I.N (l, pos), true)
        | I.D (l, pos) => (I.D (l, pos), true)
        | I.BinopExp (e1, binop, e2, pos) => 
          (case binop 
            of I.Band => let val (p1, v1) = findPprop (rettype, inlocal, lenv, env, senv, e1)
                              val (p2, v2) = findPprop (rettype, inlocal, lenv, env, senv, e2)
                          in  if v1 
                              then if v2
                                   then (I.BinopExp(p1, I.Band, p2, pos), true)
                                   else (p1, true)
                              else if v2
                              then (p2, true)
                              else (I.True, false)
                          end
             | I.Bor => let val (p1, v1) = findPprop (rettype, inlocal, lenv, env, senv, e1)
                             val (p2, v2) = findPprop (rettype, inlocal, lenv, env, senv, e2)
                         in  if v1
                             then if v2
                                  then (I.BinopExp(p1, I.Bor, p2, pos), true)
                                  else (D.showError ("transasst.fun, findPprop : "^
                                                     "There should be pprop in both sides of OR."); (I.True, false))
                             else if v2
                             then (D.showError ("transasst.fun, findPprop : "^
                                                "There should be pprop in both sides of OR."); (I.True, false))
                             else (I.True, false)
                         end
             | I.Plus => raise Fail "bug"
             | I.Minus => raise Fail "bug"
             | I.Times => raise Fail "bug"
             | I.Divide => raise Fail "bug"
             | I.Modus => raise Fail "bug"
             | I.Equ => if inlocal
                         then if hasLocalId (lenv, e1) orelse hasLocalId (lenv, e2)
                              then (I.BinopExp (e1, binop, e2, pos), true)
                              else case e1
                                    of I.Null => (I.BinopExp(e1, binop, e2, pos), true)
                                     | I.Lval(lval) =>
                                       let val t = getPlvalType (lenv, env, senv, lval)
                                       in  case t
                                            of E.Pointer _ => (I.BinopExp(e1, binop, e2, pos), true)
                                             | _ => (I.True, false)
                                       end
                                     | I.Result => let val t = case rettype
                                                                 of NONE => raise Fail "should not has \"Result\" here!"
                                                                  | SOME t' => t'
                                                    in  case t
                                                         of I.Pointer _ => (I.BinopExp(e1, binop, e2, pos), true)
                                                          | _ => (I.True, false)
                                                    end
                                     | _ => (I.True, false)
                         else (case e1
                                of  I.Null => (I.BinopExp(e1, binop, e2, pos), true)
                                  | I.Lval(lval) => let val t = getPlvalType (lenv, env, senv, lval)
                                                     in  case t
                                                          of E.Pointer _ => (I.BinopExp(e1, binop, e2, pos), true)
                                                           | _ => (I.True, false)
                                                     end
                                  | I.Result => let val t = case rettype
                                                              of NONE => raise Fail "should not has \"Result\" here!"
                                                               | SOME t' => t'
                                                 in  case t
                                                      of I.Pointer _ => (I.BinopExp(e1, binop, e2, pos), true)
                                                       | _ => (I.True, false)
                                                 end
                                  | _ => (I.True, false))
             | I.NEqu => if inlocal
                          then if hasLocalId (lenv, e1) orelse hasLocalId (lenv, e2)
                               then (I.BinopExp (e1, binop, e2, pos), true)
                               else case e1
                                     of I.Null => (I.BinopExp(e1, binop, e2, pos), true)
                                      | I.Lval(lval) => let val t = getPlvalType (lenv, env, senv, lval)
                                                         in  case t
                                                              of E.Pointer _ => (I.BinopExp(e1, binop, e2, pos), true)
                                                               | _ => (I.True, false)
                                                         end
                                      | I.Result => let val t = case rettype
                                                                  of NONE => raise Fail "should not has \"Result\" here!"
                                                                   | SOME t' => t'
                                                     in  case t
                                                          of I.Pointer _ => (I.BinopExp(e1, binop, e2, pos), true)
                                                           | _ => (I.True, false)
                                                     end
                                      | _ => (I.True, false)
                          else (case e1
                                 of  I.Null => (I.BinopExp(e1, binop, e2, pos), true)
                                   | I.Lval(lval) => let val t = getPlvalType (lenv, env, senv, lval)
                                                      in  case t
                                                           of E.Pointer _ => (I.BinopExp(e1, binop, e2, pos), true)
                                                            | _ => (I.True, false)
                                                      end
                                   | I.Result => let val t = case rettype
                                                               of  NONE => raise Fail "should not has \"Result\" here!"
                                                                 | SOME t' => t'
                                                  in  case t
                                                       of I.Pointer _ => (I.BinopExp(e1, binop, e2, pos), true)
                                                        | _ => (I.True, false)
                                                  end
                                   | _ => (I.True, false))
             | _ => if inlocal
                    then if hasLocalId (lenv, e1) orelse hasLocalId (lenv, e2)
                         then (I.BinopExp (e1, binop, e2, pos), true)
                         else (I.True, false)
                    else (I.True, false))
        | I.Not (e, pos) => if inlocal 
                             then 
                                 if hasLocalId (lenv, e) 
                                 then let val (p, v) = findPprop (rettype, true, lenv, env, senv, e)
                                      in  if v 
                                          then (I.Not(p, pos), true)
                                          else (D.showError "transasst.fun, findPprop : should has a pprop!"
                                              ; (I.True, false))
                                      end
                                 else (I.True, false) 
                             else (I.True, false)
        | I.Imply (e1, e2, pos) => (I.True, false)       
        | I.Forall (id, t, e, pos) => 
          let val newLenv = entEnv (id, lenv)  
              val (p, v) = findPprop (rettype, inlocal, lenv, env, senv, e) 
          in  if v  
              then if hasLocalId (newLenv, p) 
                   then 
                       let val (p1, v1) = findPprop (rettype, true, newLenv, env, senv, e)  
                       in  if v1
                           then (I.Forall (id, t, p1, pos), true)
                           else (D.showError "transasst.fun, findPprop : There must be a bug! should find a prop." 
                               ; (I.True, false))
                       end
                   else 
                       (p, v)
              else (I.True, false)
          end
        | I.Exists (id, t, e, pos) => 
          let val newLenv = entEnv (id, lenv) 
              val (p, v) = findPprop (rettype, inlocal, lenv, env, senv, e) 
          in  if v  
              then if hasLocalId (newLenv, p) 
                   then 
                       let val (p1, v1) = findPprop (rettype, true, newLenv, env, senv, e)  (* find this pointer prop *)
                       in  if v1
                           then (I.Exists (id, t, p1, pos), true)
                           else (D.showError "transasst.fun, findPprop : There must be a bug! should find a prop." 
                               ; (I.True, false))
                       end
                   else 
                       (p, v)
              else (I.True, false)
          end
        | I.True => (I.True, false)
        | I.False => (I.True, false)
                      
        | I.LList (e, pos) => (I.LList (e, pos), true)
        | I.Tree (e, pos) => (I.Tree (e, pos), true)
        | I.Pred (id, e, pos) => (D.showWarning "transasst.fun, findPprop : working in progress!"; (I.True, false))
        | I.Let (_, _, e3, _) =>
          findPprop (rettype, inlocal, lenv, env, senv, e3)          
        | I.Expvoid => raise Fail "invalid arguments! should be proposition!"
        | I.Null => raise Fail "invalid arguments! should be proposition!"
        | I.IntNum _ => raise Fail "invalid arguments! should be proposition!"
        | I.Prev (_, _)=> raise Fail "invalid arguments! should be proposition!"
        | I.Lval _ => raise Fail "invalid arguments! should be proposition!"
        | I.Result => raise Fail "invalid arguments! should be proposition!"



  fun transPexp (infunc, lenv, env, senv, e) = 
      case e
       of I.Expvoid => raise Fail "impossible!"
        | I.IntNum i => A.PintNum i
        | I.True => raise Fail "not exp"
        | I.False => raise Fail "not exp"
        | I.Null => A.PintNum 0
        | I.Lval lv => A.Pvar (#1(transPlval (infunc, lenv, env, senv, lv)))
        | I.BinopExp (e1, bop, e2, pos) =>
          (case bop
            of  I.Band => raise Fail "not exp"
              | I.Bor => raise Fail "not exp"
              | I.GT => raise Fail "not exp"
              | I.GE => raise Fail "not exp"
              | I.LT => raise Fail "not exp"
              | I.LE => raise Fail "not exp"
              | I.Equ => raise Fail "not exp"
              | I.NEqu => raise Fail "not exp"
              | I.Plus => let val e1' = transPexp (infunc, lenv, env, senv, e1)
                               val e2' = transPexp (infunc, lenv, env, senv, e2)
                           in  A.Pplus (e1', e2')
                           end
              | I.Minus => let val e1' = transPexp (infunc, lenv, env, senv, e1)
                                val e2' = transPexp (infunc, lenv, env, senv, e2)
                            in  A.Pminus (e1', e2')
                            end
              | I.Times => let val e1' = transPexp (infunc, lenv, env, senv, e1)
                                val e2' = transPexp (infunc, lenv, env, senv, e2)
                            in  A.Ptimes (e1', e2')
                            end
              | I.Divide => (D.showError "transasst.fun, transPexp : divide should not appear!"
                            ; A.PintNum 0)
              | I.Modus =>(D.showError "transasst.fun, transPexp : modus should not appear!"
                          ; A.PintNum 0))
        | I.Not (_, _) => raise Fail "not exp"
        | I.Result => A.Pvar (A.Preg (A.Eax))
        | I.Imply (_, _, _) => raise Fail "not exp"
        | I.Forall (_, _, _, _) => raise Fail "not exp"
        | I.Exists (_, _, _, _) => raise Fail "not exp"
        | I.Pi (_, _) => raise Fail "not exp"
        | I.N (_, _) => raise Fail "not exp"
        | I.D (_, _) => raise Fail "not exp"
        | I.Prev (e, _) => (D.showError "transasst.fun, transPexp : We haven't delt with this case"
                           ; A.Pvar(#1(transPlval (infunc, lenv, env, senv, e))))
        | I.LList (_, _) => raise Fail "not exp"
        | I.Tree (_, _) => raise Fail "not exp"
        | I.Pred (_, _, _) => raise Fail "not exp"
        | I.Let (_, _, _, _) => raise Fail "not exp"
      
                                     
  fun transPprop (infunc, lenv, env, senv, p) =
      case p
       of I.Expvoid => raise Fail "impossible!"
        | I.IntNum i => raise Fail "not a pprop"
        | I.True => A.Ptrue
        | I.False => A.Pnot (A.Ptrue)
        | I.Null => raise Fail "not a pprop"
        | I.Lval lv => raise Fail "not a pprop"
        | I.BinopExp (e1, bop, e2, pos) => 
          (case bop
            of  I.Band => A.Pand (transPprop (infunc, lenv, env, senv, e1), transPprop (infunc, lenv, env, senv, e2))
              | I.Bor => A.Por (transPprop (infunc, lenv, env, senv, e1), transPprop (infunc, lenv, env, senv, e2))
              | I.GE => A.Pge (transPexp (infunc, lenv, env, senv, e1), transPexp (infunc, lenv, env, senv, e2))
              | I.GT => A.Pgt (transPexp (infunc, lenv, env, senv, e1), transPexp (infunc, lenv, env, senv, e2))
              | I.LE => A.Ple (transPexp (infunc, lenv, env, senv, e1), transPexp (infunc, lenv, env, senv, e2))
              | I.LT => A.Plt (transPexp (infunc, lenv, env, senv, e1), transPexp (infunc, lenv, env, senv, e2))
              | I.Equ => A.Peq (transPexp (infunc, lenv, env, senv, e1), transPexp (infunc, lenv, env, senv, e2))
              | I.NEqu => A.Pne (transPexp (infunc, lenv, env, senv, e1), transPexp (infunc, lenv, env, senv, e2))
              | I.Plus => raise Fail "not a pprop"  
              | I.Minus => raise Fail "not a pprop"  
              | I.Times => raise Fail "not a pprop"  
              | I.Divide => raise Fail "not a pprop"  
              | I.Modus => raise Fail "not a pprop")  
        | I.Not (e, pos) => A.Pnot (transPprop (infunc, lenv, env, senv, e))
        | I.Result => raise Fail "not a pprop"
        | I.Imply(_, _, _) => (D.showError "transasst.fun, transPprop : No this case in Pointer logic!"
                              ; A.Ptrue)
        | I.Forall (id, t, e, pos) =>
          let val newLenv = entEnv (id, lenv)
              val newt = transType t
              val newp = transPprop (infunc, newLenv, env, senv, e)
          in  A.Pforall ((id, newt), newp)
          end
        | I.Exists (id, t, e, pos) =>
          let val newLenv = entEnv (id, lenv)
              val newt = transType t
              val newp = transPprop (infunc, newLenv, env, senv, e)
          in  A.Pex ((id, newt), newp)
          end
        | I.Pi (ll, pos) =>
          let val f = fn lv => #1(transPlval (infunc, lenv, env, senv, lv))
              val g = fn l => List.map f l
          in  A.Pi (List.map g ll)
          end
        | I.N (l, pos) => 
          let val f = fn lv => #1(transPlval (infunc, lenv, env, senv, lv))
          in  A.N (List.map f l)
          end
        | I.D (l, pos) =>
          let val f = fn lv => #1(transPlval (infunc, lenv, env, senv, lv))
          in  A.D (List.map f l)
          end
        | I.Prev (_, _) => raise Fail "not a pprop"
        | I.LList (e, pos) => A.Plist (transPexp (infunc, lenv, env, senv, e))
        | I.Tree (e, pos) => A.Ptree (transPexp (infunc, lenv, env, senv, e))
        | I.Pred (id, e, pos) => (D.showWarning "transasst.fun, transPprop : working in progress!"
                                 ; A.Ppred (id, transPprop (infunc, lenv, env, senv, e)))
        | I.Let (e1, e2, e3, pos) => (D.showWarning "transasst.fun, transPprop : should not appear here!"
                                     ; transPprop (infunc, lenv, env, senv, e3))

  fun transPassert (rettype, infunc, env, senv, exp) : A.passert = 
      let val empe = empEnv ()
          val (selp, valid) = findPprop (rettype, false, empe, env, senv, exp)
      in  if valid
          then let val newp = transPprop (infunc, empe, env, senv, selp)
               in  SOME newp
               end
          else NONE
      end

  fun types2etype ty =
      (case ty
        of  E.Simple => A.Int
          | E.Struct s => A.Str s
          | E.Pointer t => A.Ptr (types2etype t)
          | E.Array (i, t) => (D.showError "transasst.fun, types2etype : Does not support Array type now!"
                             ; A.Int))

  fun transEnv (hasRet, (id, (islocal, offset, types))) =
      let val etype = types2etype types
      in  if islocal
          then let val aptr = A.Pstk(offset, A.Ebp)
                   val aptr2 = A.Pstk(offset - 4*hasRet, A.Esp) 
               in  (aptr, aptr2, etype)
               end
          else let val aptr = A.Pgmem (mapToMem id) 
               in  (aptr, aptr, etype)
               end
      end

  fun topSEnv (senv : (int * E.types) E.struct_env) =
      let fun f (i, ty) = (i, types2etype ty)
      in  E.transSenv (f, senv)
      end

  fun topEnv (hasRet : int, env : (bool * int * E.types) E.env)=
      let val elist = E.toList env
          fun f oneenv = transEnv (hasRet, oneenv)
          val asmenv = List.map f elist
      in  asmenv
      end

  fun top (rettype, expopt, infunc, env, senv) =
      case expopt 
       of NONE => NONE
        | SOME exp =>
          let val passert : A.passert = transPassert (rettype, infunc, env, senv, exp)
              val lenv = empEnv ()
              val assert = transProp (rettype, exp, infunc, lenv, env, senv)
          in  SOME (assert, passert)
          end
end
